Problem:
 concat(leaf(),Y) -> Y
 concat(cons(U,V),Y) -> cons(U,concat(V,Y))
 lessleaves(X,leaf()) -> false()
 lessleaves(leaf(),cons(W,Z)) -> true()
 lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))

Proof:
 Complexity Transformation Processor:
  strict:
   concat(leaf(),Y) -> Y
   concat(cons(U,V),Y) -> cons(U,concat(V,Y))
   lessleaves(X,leaf()) -> false()
   lessleaves(leaf(),cons(W,Z)) -> true()
   lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [true] = 0,
     
     [false] = 0,
     
     [lessleaves](x0, x1) = x0 + x1 + 28,
     
     [cons](x0, x1) = x0 + x1 + 7,
     
     [concat](x0, x1) = x0 + x1 + 49,
     
     [leaf] = 15
    orientation:
     concat(leaf(),Y) = Y + 64 >= Y = Y
     
     concat(cons(U,V),Y) = U + V + Y + 56 >= U + V + Y + 56 = cons(U,concat(V,Y))
     
     lessleaves(X,leaf()) = X + 43 >= 0 = false()
     
     lessleaves(leaf(),cons(W,Z)) = W + Z + 50 >= 0 = true()
     
     lessleaves(cons(U,V),cons(W,Z)) = U + V + W + Z + 42 >= U + V + W + Z + 126 = lessleaves(concat(U,V),concat(W,Z))
    problem:
     strict:
      concat(cons(U,V),Y) -> cons(U,concat(V,Y))
      lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
     weak:
      concat(leaf(),Y) -> Y
      lessleaves(X,leaf()) -> false()
      lessleaves(leaf(),cons(W,Z)) -> true()
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [true] = 0,
       
       [false] = 0,
       
       [lessleaves](x0, x1) = x0 + x1,
       
       [cons](x0, x1) = x0 + x1 + 1,
       
       [concat](x0, x1) = x0 + x1,
       
       [leaf] = 0
      orientation:
       concat(cons(U,V),Y) = U + V + Y + 1 >= U + V + Y + 1 = cons(U,concat(V,Y))
       
       lessleaves(cons(U,V),cons(W,Z)) = U + V + W + Z + 2 >= U + V + W + Z = lessleaves(concat(U,V),concat(W,Z))
       
       concat(leaf(),Y) = Y >= Y = Y
       
       lessleaves(X,leaf()) = X >= 0 = false()
       
       lessleaves(leaf(),cons(W,Z)) = W + Z + 1 >= 0 = true()
      problem:
       strict:
        concat(cons(U,V),Y) -> cons(U,concat(V,Y))
       weak:
        lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
        concat(leaf(),Y) -> Y
        lessleaves(X,leaf()) -> false()
        lessleaves(leaf(),cons(W,Z)) -> true()
      Bounds Processor:
       bound: 1
       enrichment: match
       automaton:
        final states: {6,5}
        transitions:
         cons1(3,11) -> 11*
         cons1(4,8) -> 8,5
         cons1(4,10) -> 8,5
         cons1(1,8) -> 8,5
         cons1(1,10) -> 8,5
         cons1(2,11) -> 11*
         cons1(3,8) -> 8,5
         cons1(3,10) -> 8,5
         cons1(4,11) -> 11*
         cons1(1,11) -> 11*
         cons1(2,8) -> 8,5
         cons1(2,10) -> 8,5
         concat1(3,1) -> 8*
         concat1(3,3) -> 8*
         concat1(3,11) -> 11*
         concat1(4,2) -> 8*
         concat1(4,4) -> 8*
         concat1(4,8) -> 11*
         concat1(4,10) -> 11*
         concat1(1,2) -> 8*
         concat1(1,4) -> 8*
         concat1(1,8) -> 11*
         concat1(1,10) -> 11*
         concat1(2,1) -> 8*
         concat1(2,3) -> 10*
         concat1(2,11) -> 11*
         concat1(3,2) -> 8*
         concat1(3,4) -> 8*
         concat1(3,8) -> 11*
         concat1(3,10) -> 11*
         concat1(4,1) -> 8*
         concat1(4,3) -> 10*
         concat1(4,11) -> 11*
         concat1(1,1) -> 8*
         concat1(1,3) -> 8*
         concat1(1,11) -> 11*
         concat1(2,2) -> 8*
         concat1(2,4) -> 8*
         concat1(2,8) -> 11*
         concat1(2,10) -> 11*
         true1() -> 6*
         lessleaves1(8,11) -> 6*
         lessleaves1(10,11) -> 6*
         lessleaves1(11,8) -> 6*
         lessleaves1(11,10) -> 6*
         lessleaves1(11,11) -> 6*
         false1() -> 6*
         concat0(3,1) -> 5*
         concat0(3,3) -> 5*
         concat0(4,2) -> 5*
         concat0(4,4) -> 5*
         concat0(1,2) -> 5*
         concat0(1,4) -> 5*
         concat0(2,1) -> 5*
         concat0(2,3) -> 5*
         concat0(3,2) -> 5*
         concat0(3,4) -> 5*
         concat0(4,1) -> 5*
         concat0(4,3) -> 5*
         concat0(1,1) -> 5*
         concat0(1,3) -> 5*
         concat0(2,2) -> 5*
         concat0(2,4) -> 5*
         cons0(3,1) -> 1*
         cons0(3,3) -> 1*
         cons0(4,2) -> 1*
         cons0(4,4) -> 1*
         cons0(1,2) -> 1*
         cons0(1,4) -> 1*
         cons0(2,1) -> 1*
         cons0(2,3) -> 1*
         cons0(3,2) -> 1*
         cons0(3,4) -> 1*
         cons0(4,1) -> 1*
         cons0(4,3) -> 1*
         cons0(1,1) -> 1*
         cons0(1,3) -> 1*
         cons0(2,2) -> 1*
         cons0(2,4) -> 1*
         lessleaves0(3,1) -> 6*
         lessleaves0(3,3) -> 6*
         lessleaves0(4,2) -> 6*
         lessleaves0(4,4) -> 6*
         lessleaves0(5,5) -> 6*
         lessleaves0(1,2) -> 6*
         lessleaves0(1,4) -> 6*
         lessleaves0(2,1) -> 6*
         lessleaves0(2,3) -> 6*
         lessleaves0(3,2) -> 6*
         lessleaves0(3,4) -> 6*
         lessleaves0(4,1) -> 6*
         lessleaves0(4,3) -> 6*
         lessleaves0(1,1) -> 6*
         lessleaves0(1,3) -> 6*
         lessleaves0(2,2) -> 6*
         lessleaves0(2,4) -> 6*
         leaf0() -> 2*
         false0() -> 6,3
         true0() -> 6,4
         1 -> 5,8
         2 -> 5,8
         3 -> 10,5
         4 -> 5,8
         8 -> 11*
         10 -> 11*
       problem:
        strict:
         
        weak:
         concat(cons(U,V),Y) -> cons(U,concat(V,Y))
         lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
         concat(leaf(),Y) -> Y
         lessleaves(X,leaf()) -> false()
         lessleaves(leaf(),cons(W,Z)) -> true()
       Qed